feat(Combinatorics/SimpleGraph/Inversion): add Möbius inversion between copy counts and induced copy counts#36
Open
FordUniver wants to merge 3 commits into
Open
Conversation
FordUniver
changed the title
FordUniver
force-pushed
the
feat/copy-mobius
branch
from
2b4e2dd to
734f28f
Compare
FordUniver
changed the base branch from
feat/simplegraph-aut
to
diffbase/copy-mobius
FordUniver
force-pushed
the
feat/copy-mobius
branch
3 times, most recently
from
b664e44 to
d9da9e5
Compare
FordUniver
force-pushed
the
diffbase/copy-mobius
branch
from
fa6e3bb to
3ae9341
Compare
FordUniver
force-pushed
the
feat/copy-mobius
branch
4 times, most recently
from
ac4cb3d to
57f3d6b
Compare
…opy counts and induced copy counts Adds the bijection `Copy.equivSigmaEmbedding`, the labelled forward count identity `copyCount_eq_sum_embeddingCount`, and its Möbius inverse `embeddingCount_eq_sum_signed_copyCount` over ℤ. The Möbius direction reduces via the order-equivalence `iccEquivPowersetEdgeFinsetSdiff` between `Icc G K` and the powerset of the edge difference to `Finset.sum_powerset_neg_one_pow_card`. Supporting `Copy.inducedShape` (the pullback `H.comap f.toEmbedding`) and the per-fiber bijection `Copy.fiberInducedShapeEquiv` are kept inline in this file rather than split out, since neither has a standalone consumer outside this Möbius decomposition. Co-authored-by: Malte Jackisch <45597826+MaltyBlanket@users.noreply.github.com>
Clean-slate restructure now complete: * `edgeSetSdiffFinset G K` constructed via `Set.Finite.toFinset` — no per-graph `Fintype` synthesis required. * `natCard_edgeSet_eq_add_card_sdiff` (cardinality bridge): proved via `Set.ncard_diff_add_ncard_of_subset` + `Nat.card_coe_set_eq` / `Set.ncard_eq_toFinset_card`. * `iccEquivPowersetEdgeFinsetSdiff`: `left_inv` / `right_inv` proved by case-splitting on `fromEdgeSet_adj` membership and using the diag-freeness of edges in `K`. * Kernel split into degenerate (`Icc G G`, trivial) and strict (`G < L`, reindex + powerset alternating sum + non-empty extra-edge finset). * Main theorem: substitute forward identity, distribute, swap sums, factor, apply `Finset.sum_eq_single G` with the strict case discharging non-`G` terms. Zero `sorry`, zero `Classical.decRel`, zero `open Classical in`, zero `attribute [local instance]` in the file. All decidability requirements satisfied by `Set.Finite.toFinset` (noncomputable but Classical-free at the source level) and the bridge `Nat.card_coe_set_eq`.
FordUniver
force-pushed
the
diffbase/copy-mobius
branch
from
3ae9341 to
5372c30
Compare
FordUniver
force-pushed
the
feat/copy-mobius
branch
from
57f3d6b to
e8e1731
Compare
…er catch-up
Rename Set.{mem_diff,diff_eq_empty,ncard_diff_add_ncard_of_subset} to the
sdiff spellings; omit unused DecidableEq/DecidableLE section vars on the
edgeSetSdiffFinset helpers; weaken edgeSet_sdiff_finite's Fintype V to Finite V
per the unusedFintypeInType linter.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the bijection
Copy.equivSigmaEmbeddingdecomposing every copy ofGinHas a choice of induced shapeG' ∈ Icc G ⊤together with an embeddingG' ↪g H, and derives the labelled count identities: a forward sumH.copyCount G = ∑ G' ∈ Icc G ⊤, H.embeddingCount G'and its Möbius inverse overℤwith sign(-1) ^ #(G'.edgeFinset \ G.edgeFinset). The Möbius direction reduces via the order-equivalenceiccEquivPowersetEdgeFinsetSdiffbetweenIcc G Kand the powerset of the edge difference toFinset.sum_powerset_neg_one_pow_card. Supporting material onCopy.inducedShape(the pullbackH.comap f.toEmbedding) and the per-fiber bijectionCopy.fiberInducedShapeEquivlives in the same file rather than being split out, since neither has a standalone consumer outside this Möbius decomposition.Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com
Came up while preparing density-level versions of the same identity for a downstream flag-algebras formalisation. The labelled count version, stated over ℤ for the signs, is the standalone-mergeable kernel; density transports (over ℚ, dividing by descending-factorials or binomial coefficients) and unlabelled-count variants follow in separate PRs.
UnlabeledEmbedding,unlabeledEmbeddingCountandembeddingCountleanprover-community/mathlib4#38631Diff for the changes just in this PR over its predecessors: link